Nuprl Lemma : ecl-trans-state-from-append 11,40
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple{i:l}(ds; da), z:top, L1,L2:(top List).
sqequal(ecl-trans-state-from(v; z; append(L1; L2));
sqequal(ecl-trans-state-from(v; ecl-trans-state-from(v; z; L1); L2)) 
latex

Definitionsspreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-tuple{i:l}(ds; da), t  T, top, x,y. t(x;y), x:A. B(x), ecl-trans-state-from(v; z; L), Id, x. t(x), fpf(A; a.B(a)), Knd
Lemmastop wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, list accum append

origin